Inference at * 1 
Iof proof for Lemma bij imp exists inv:



1. A : Type
2. B : Type
3. f : AB
4. Bij(A;B;f)
  g:BA. InvFuns(A;B;f;g) 

latex

 by ((Repeat (Unfolds ``biject inject surject`` 4)) 
CollapseTHEN (D 4)) 

latex

C1: 

C1: 4. a1, a2:A. (f(a1) = f(a2))  (a1 = a2)
C1: 5. b:B. a:A. (f(a) = b)
C1:   g:BA. InvFuns(A;B;f;g)
C.

Definitions

Surj(A;B;f), Inj(A;B;f), P & Q, Bij(A;B;f)